Nuprl Lemma : mapfilter_wf
11,40
postcript
pdf
T
:Type,
P
:(
T
),
T'
:Type,
f
:({
x
:
T
|
(
P
(
x
))}
T'
),
L
:(
T
List).
mapfilter(
f
;
P
;
L
)
(
T'
List)
latex
Definitions
mapfilter(
f
;
P
;
L
)
,
t
T
,
x
:
A
.
B
(
x
)
,
prop{i:l}
Lemmas
bool
wf
,
assert
wf
,
map
wf
,
filter
type
origin
T:Type, P:(T
), T':Type, f:({x:T| 
(P(x))} T'), L:(T List).
(T' List) T:Type, P:(T), T':Type, f:({x:T| (P(x))} T'), L:(T List).
(T' List) Tx:A. B(x)